\begin{tabbing}
$\forall$\=$A$:Type, $I$:MaInterface($A$), $l$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]${\it nmr}$:Namer(2;[${\it tg}$; lname($l$)] @ ma{-}interface{-}tags($I$)).
\-\\[0ex]Normal($A$,$I$)
\\[0ex]$\Rightarrow$ gluable($I$;$l$;${\it tg}$)
\\[0ex]$\Rightarrow$ gluable2($A$;$I$;$l$;${\it tg}$)
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id.\+
\\[0ex]($x$ $\in$ filter($\lambda$$i$.$\neg_{b}$$i$ = source($l$);remove{-}repeats(IdDeq;ma{-}interface{-}locs($I$))))
\\[0ex]$\Rightarrow$ (\=triggersGlue(\=$A$;\+\+
\\[0ex](link ${\it nmr}$(0) from $x$ to source($l$));
\\[0ex](${\it nmr}$(1));
\\[0ex]ma{-}interface{-}ds($I$;$x$);
\\[0ex]($I$($x$).2))
\-\\[0ex]$\in$ Realizer))
\-\-
\end{tabbing}